package org.eclipse.iota.rules;

import java.util.List;

import org.eclipse.iota.IotaPackage;
import org.eclipse.iota.assignments.Assignment;
import org.eclipse.iota.assignments.RangeAssignmentGenerator;
import org.eclipse.iota.bounds.IotaBoundUtil;
import org.eclipse.iota.evaluator.IotaConstantEvaluator;
import org.eclipse.iota.evaluator.IotaEvaluator.EvaluationException;
import org.eclipse.iota.model.Alternation;
import org.eclipse.iota.model.Boolean;
import org.eclipse.iota.model.Clause;
import org.eclipse.iota.model.Constant;
import org.eclipse.iota.model.Equation;
import org.eclipse.iota.model.EquationType;
import org.eclipse.iota.model.Existential;
import org.eclipse.iota.model.Expression;
import org.eclipse.iota.model.LinearExpression;
import org.eclipse.iota.model.Reference;
import org.eclipse.iota.model.Variable;
import org.eclipse.iota.rewrite.AbstractSymmetricRule;
import org.eclipse.iota.util.IotaCopyUtil;
import org.eclipse.iota.util.IotaFindUtil;
import org.eclipse.iota.util.IotaVariableUtil;

/**
 * @author Christian Krause
 * @generated NOT
 */
public class LinearExponentiation extends AbstractSymmetricRule {
	
	/**
	 * @param expression Expression.
	 * @param linear Linear expression.
	 */
	public boolean applySymmetric(Expression expression, LinearExpression linear, boolean change) {
		
		// Check the factor of the linear expression and create the range assignments.
		Constant factor = linear.getFactor();
		RangeAssignmentGenerator assignments = getRangeAssignments(expression, factor.getValue().intValue());
		if (assignments==null) return false;
		
		// Get the clause.
		Clause clause = expression.getEquation().getClause();
		Alternation alternation = clause.getAlternation();
		
		// An evaluator.
		IotaConstantEvaluator evaluator = new IotaConstantEvaluator();
		evaluator.setModulus(factor);
		boolean matched = false, replaced = false;
		
		for (Assignment assignment : assignments) {
			
			// Evaluate the expression given the current assignment.
			Constant offset = null;
			try {
				evaluator.setAssignment(assignment);
				offset = evaluator.evaluate(expression);
			} catch (EvaluationException e) {
				return false; // Rule cannot be applied.
			}
			
			// If this is the same as the offset of the linear expression, we have a match.
			if (linear.getOffset().isEqualTo(offset)) {
				
				// We have a match.
				matched = true;

				// Make a copy of the current clause.
				Clause copy = IotaCopyUtil.copy(clause);
				
				for (Variable target : assignments.getVariables()) {

					// Create a fresh variable.
					Existential fresh = IotaVariableUtil.freshExistential(
											copy.getAlternation()!=null ? copy : clause);
					
					// Compute the linear equation.
					Equation equation = getLinearEquation(target, fresh, factor, offset);
					
					// Check if there is already such a variable + equation.
					if (IotaVariableUtil.findSuchThat(clause, fresh, equation)==null) {
						
						// Add the new clause to the property.
						copy.getExistentials().add(fresh);
						copy.getConstraints().add(equation);
						
						if (change) {
							copy.setAlternation(alternation);
						}
						
						// Also add a constraint for the new existential.
						if (IotaBoundUtil.isPositive(new Reference(target), copy) &&
							factor.isPositive() && !offset.isNegative()) {							
							Equation range = new Equation(new Reference(fresh), new Reference(target), EquationType.LESS);
							range.setInferred(true);
							copy.getConstraints().add(range);
						}
						
						replaced = true;					
					}
				}
				
			}
		}
		
		if (change) {
			if (replaced) {

				// Remove the original clause.
				alternation.getClauses().remove(clause);

				// Automatically infer variable relations.
				//applyRule(UpdateBounds.class);
				return true;

			} else if (!matched && !IotaFindUtil.contains(clause, new Boolean(false))) {

				// None of the cases matched, so there is no possible solution.
				clause.getConstraints().add(new Boolean(false));
				return true;
			}
		}
		return false;
		
	}
	
	
	/*
	 * Initialize a range assignments object.
	 */
	private RangeAssignmentGenerator getRangeAssignments(Expression expression, int factor) {
		
		// Check some preconditions.
		if (factor==-1 || factor==0 || factor==1) return null;
		
		// Get a list of used variables first.
		List<Variable> variables = IotaVariableUtil.getUsedVariables(expression);		
		if (IotaFindUtil.getAllExpressions(expression, IotaPackage.eINSTANCE.getReference()).isEmpty()) return null;
		if (IotaFindUtil.getAllExpressions(expression, IotaPackage.eINSTANCE.getExponentiation()).isEmpty()) return null;
		if (!IotaFindUtil.getAllExpressions(expression, IotaPackage.eINSTANCE.getDivision()).isEmpty()) return null;
		
		if (factor<0) {
			return new RangeAssignmentGenerator(variables, factor+1, 0);
		} else {
			return new RangeAssignmentGenerator(variables, 0, factor-1);			
		}
	}
	
	
	/*
	 * Create a new equation of the shape [target = factor*base + offset]
	 */
	private Equation getLinearEquation(Variable target, Variable base, Constant factor, Constant offset) {
		
		// Create the linear combination.
		LinearExpression linear = new LinearExpression();
		linear.setBase(new Reference(base));
		linear.setFactor(factor.copy());
		linear.setOffset(offset.copy());
		
		// Create the equation.
		Equation equation = new Equation(new Reference(target), linear.toBasic());
		equation.setInferred(true);
		return equation;
		
	}
	
}
